Nuprl Definition : finite
4,23
postcript
pdf
finite(
T
) ==
f
:(
T
T
). Inj(
T
;
T
;
f
)
Surj(
T
;
T
;
f
)
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
Inj(
A
;
B
;
f
)
,
Surj(
A
;
B
;
f
)
FDL editor aliases
finite
origin
f:(T
T). Inj(T; T; f) 
Surj(T; T; f) f:(TT). Inj(T; T; f) Surj(T; T; f) x:A. B(x) Q